FDL - Nuprl Definition : d-single-init

Nuprl Definition : d-single-init

@i: x:T initially x = v(j) == if eqof(IdDeq)(j,i) then x : T initially x = v else fi

Definitions x.A(x), if b then t else f fi , f(a), eqof(d), IdDeq, x : t initially x = v,

FDL editor aliases d-single-init

Definitions	x.A(x), if b then t else f fi , f(a), eqof(d), IdDeq, x : t initially x = v,
FDL editor aliases	d-single-init